$\forall$${\it es}$:ES, $P$, $Q$, ${\it P'}$, ${\it Q'}$:(E$\rightarrow\mathbb{P}$), $f$:(\{$e$:E$\mid$ $P$($e$)\} $\rightarrow$\{$e$:E$\mid$ $Q$($e$)\} ).
\\[0ex]$P$ $\Leftarrow\!\Rightarrow$ ${\it P'}$ $\Rightarrow$ $Q$ $\Leftarrow\!\Rightarrow$ ${\it Q'}$ $\Rightarrow$ ($Q$ $\leftarrow$==$f$== $P$ $\Leftarrow\!\Rightarrow$ ${\it Q'}$ $\leftarrow$==$f$== ${\it P'}$)